the_w:World, e:E, t:.
FairFifo
 (isrcv(kind(e)))
 (match(lnk(kind(e));t;time(e)))
 (msg(a(loc(e);time(e)))  onlnk(lnk(kind(e));m(source(lnk(kind(e)));t))) 

latex

Definitions	x:A. B(x), , P  Q, t  T, SQType(T), {T}, , (x  l), x:A. B(x), A c B, {i..j}, P & Q, i  j < k
Lemmas	better-w-match-exists, w-match-unique, le wf, assert wf, w-match wf, lnk wf, w-ekind wf, w-time wf, isrcv wf, fair-fifo wf, nat wf, w-E wf, world wf, length wf1, w-action wf, ldst wf, w-rcvs wf, w-Msg wf, w-snds wf